Skip to content

feat: lemmas about iterator collectors #8380

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 7 commits into from
May 21, 2025
Merged

feat: lemmas about iterator collectors #8380

merged 7 commits into from
May 21, 2025

Conversation

datokrat
Copy link
Contributor

@datokrat datokrat commented May 16, 2025 •
edited
Loading

This PR provides simple lemmas about toArray, toList and toListRev for the iterator library.

It also changes the definition of Iter and IterM so that they aren't equal anymore and in particular not definitionally equal. While it was very convenient to have them be definitionally equal when working with dependent code, it was also confusing and annoying that one would sometimes end up with something like it.toList = IterM.toList it, where it : Iter β.

@datokrat datokrat added the changelog-library Library label May 16, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 16, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 16, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 60ea92fdb0594065072ed843724d98cd15b76fba --onto ca9b3eb75f3f794d3d526a7c37da389175b317a2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-16 14:30:37)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 60ea92fdb0594065072ed843724d98cd15b76fba --onto efe2ab4c04e81fe2a3edcc0d861449490b4431b2. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-20 07:51:08)
  • ✅ Mathlib branch lean-pr-testing-8380 has successfully built against this PR. (2025-05-20 14:27:51) View Log
  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-05-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-21 15:49:56)

@datokrat datokrat marked this pull request as ready for review May 16, 2025 14:31
@datokrat datokrat requested a review from TwoFX as a code owner May 16, 2025 14:31
@datokrat datokrat force-pushed the paul/iterators/1 branch from 13f5672 to 5334da1 Compare May 20, 2025 07:16
TwoFX
TwoFX reviewed May 20, 2025
View reviewed changes
@datokrat datokrat force-pushed the paul/iterators/1 branch from e55175d to 9e0c59e Compare May 20, 2025 12:25
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8380
463adec
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8380
e34f5e4
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 20, 2025
@datokrat datokrat marked this pull request as draft May 21, 2025 15:15
@datokrat datokrat force-pushed the paul/iterators/1 branch from 9e0c59e to ed1da9d Compare May 21, 2025 15:18
@datokrat datokrat force-pushed the paul/iterators/initial-for-1 branch from 767c578 to 47a1355 Compare May 21, 2025 15:18
@datokrat datokrat marked this pull request as ready for review May 21, 2025 15:19
@datokrat datokrat changed the base branch from paul/iterators/initial-for-1 to master May 21, 2025 21:10
@datokrat datokrat added this pull request to the merge queue May 21, 2025
Merged via the queue into master with commit 0a43c13 May 21, 2025
23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX approved these changes

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@datokrat @leanprover-community-bot @TwoFX